R-names(A)
== case A of 
== Rnone => []
== Rplus(left,right)=>rec1,rec2.rec1 @ rec2
== Rinit(loc,T,x,v)=> [(inr <loc, x> )]
== Rframe(loc,T,x,L)=> [(inr <loc, x> )]
== Rsframe(lnk,tag,L)=> [(inl locknd(destination(lnk);rcv(lnk,tag)) )]
== Reffect(loc,ds,knd,T,x,f)=> [(inl locknd(loc;knd) ); 

== Reffect(loc,ds,knd,T,x,f)=> [(inr <loc, x> ) / map(x.inr <loc, x> ;fpf-domain(ds))]
== Rsends(ds,knd,T,l,dt,g)=> [(inl locknd(source(l);knd) ) / 
== Rsends(ds,knd,T,l,dt,g)=> [(map(x.inr <source(l), x> ;fpf-domain(ds))
== Rsends(ds,knd,T,l,dt,g)=> [@ map(tg.inl locknd(destination(l);rcv(l,tg)) 
== Rsends(ds,knd,T,l,dt,g)=> [@ map;remove-repeats(IdDeq;fpf-domain(dt) @ map(x.x.1;g))))]
== Rpre(loc,ds,a,T,P)=> [(inl locknd(loc;locl(a)) ) / map(x.inr <loc, x> ;fpf-domain(ds))]
== Rkframe(loc,k,L)=> [(inl locknd(loc;k) )]
== Rksframe(loc,k,L)=> [(inl locknd(loc;k) )]
== Rrframe(loc,x,L)=> [(inr <loc, x> )] 

latex

---

clarification:

R-names(A)
== case A of 
== Rnone => []
== Rplus(left,right)=>rec1,rec2.rec1 @ rec2
== Rinit(loc,T,x,v)=> [(inr <loc, x> ) / []]
== Rframe(loc,T,x,L)=> [(inr <loc, x> ) / []]
== Rsframe(lnk,tag,L)=> [(inl locknd(destination(lnk);rcv(lnk,tag)) ) / []]
== Reffect(loc,ds,knd,T,x,f)=> [(inl locknd(loc;knd) ); 

== Reffect(loc,ds,knd,T,x,f)=> [(inr <loc, x> ) / map(x.inr <loc, x> ;fpf-domain(ds))]
== Rsends(ds,knd,T,l,dt,g)=> [(inl locknd(source(l);knd) ) / 
== Rsends(ds,knd,T,l,dt,g)=> [(map(x.inr <source(l), x> ;fpf-domain(ds))
== Rsends(ds,knd,T,l,dt,g)=> [@ map(tg.inl locknd(destination(l);rcv(l,tg)) 
== Rsends(ds,knd,T,l,dt,g)=> [@ map;remove-repeats(IdDeq;fpf-domain(dt) @ map(x.x.1;g))))]
== Rpre(loc,ds,a,T,P)=> [(inl locknd(loc;locl(a)) ) / map(x.inr <loc, x> ;fpf-domain(ds))]
== Rkframe(loc,k,L)=> [(inl locknd(loc;k) ) / []]
== Rksframe(loc,k,L)=> [(inl locknd(loc;k) ) / []]
== Rrframe(loc,x,L)=> [(inr <loc, x> ) / []] 

latex

Definitions	es realizer ind, source(l), destination(l), rcv(l,tg), remove-repeats(eq;L), IdDeq, as @ bs, t.1, locl(a), map(f;as), x.A(x), fpf-domain(f), inl x , locknd(i;k), [car / cdr], inr x , <a, b>, []
FDL editor aliases	R-names